In this section we first show that \rsd nets meet some general properties, then we focus on the reachability problem and we show that reachability is decidable for this class of Petri nets.
We start by recalling the definition of reachability:

\begin{definition}
 A marking $m$ is \emph{reachable} if there exists a firing sequence $t_1, \dots, t_n$ such that 
 $$m_0 \rightarrow_{t_1} \dots \rightarrow_{t_n} m$$
 also denoted $m_0 \rightarrow^* m$.
 
 Given a Petri net with timestamps $TS$ and a marking $m$, the \emph{reachability problem} consists in checking whether $m$ is reachable in $TS$. 
\end{definition}


\subsection{General Properties}
We now show that \rsd nets are 1-safe:
\begin{definition}
 A Petri net is \emph{1-safe} if each place contains at most one token in each reachable marking. 
\end{definition}

The proof follows by observing that the initial marking is 1-safe by construction and then applying an ease induction on the length of the firing sequence.

\begin{lemma}\label{lem:m0}
 Marking $m_0$ in \rsd nets is 1-safe.
\end{lemma}
\begin{proof}
 Follows by definition \ref{def:rs}.
\end{proof}

Next lemma shows that if $m$ is a 1-safe marking then, for each enabled transition $t$, marking $m'$ such that $\firing{m}{t}{m'}$ is 1-safe.

\begin{lemma}\label{lem:m}
 Let $m$ be a 1-safe marking in a \rsd net $TS$. For each enabled transition $t$ in $m$, marking $m'$ such that  $\firing{m}{t}{m'}$ is 1-safe.
\end{lemma}
\begin{proof}
 The proof proceeds by a case analysis on the type of enabled transition. By construction there are two types of transition: the transition of the clock $t_c$ and transitions that correspond to reactions $t_r$.
 \begin{description}
  \item[$t_c$] This transition is always enabled. It consumes a token from all places and recreates it with the characteristics specified by guard $L(t_c)$. This way as $m$ is a 1-safe marking and as all tokens are consumed and recreated by the firing, $m'$ is 1-safe. This concludes the analysis of this case.
  \item[$t_r$] This transition is enabled iff $$\bigwedge_{S_i \in (R \cup I)}(z-\birth_i \geq \dur(r)) \ \wedge 
\bigwedge_{P_k \in P}\big [ (\bool_k=0 \wedge \birth_k' = z) \vee (\bool_k=1 \wedge \birth_k' = \birth_k) \big].$$
Notice that $\pre{t_r} = \post{t_r}$, thus for each place involved in the transition we first consume one of his tokens and then we immediately recreate it. Thus by recalling that $m$ is 1-safe, we can immediately conclude that $m'$ is 1-safe as well. Thus completing the analysis of this case and the proof.
 \end{description}

\end{proof}


% 
% 
% \begin{lemma}[Invariant Lemma]
%  For each place $p \in P \setminus \{\Pclock\}$ if $p$ encodes a living resource then $M(p) = \tuple{1, n,m}$ and $n \geq m$, otherwise if $p$ represents a dead resource $M(p) = \tuple{0, n, 0}$. 
% Moreover, for each place $p \in P $ $M'(p) = L_{\rho}(t,p)$.
% \end{lemma}
We are now ready to state the main result of this section:

\begin{theorem}[One Safe]
  \rsd nets  with initial marking $m_0$ are \emph{one safe}.
\end{theorem}
\begin{proof}
The proof follows by induction on the length of firing sequences.
We know that $m_0$ is 1-safe (cfr. Lemma \ref{lem:m0}). Let $m$ be a reachable marking in a \rsd net $TS$. Hence we have 
$$m_0 \rightarrow_{t_1} \dots \rightarrow_{t_n} m$$
By inductive hypothesis we know that all markings reachable with firing sequences of length $n-1$ are 1-safe. By applying Lemma \ref{lem:m} we can deduce that $m$ is 1-safe, thus concluding the proof of the theorem.
\end{proof}

% 
% 
% \begin{corollary}
%  A place $p \in P \setminus \{\Pclock\}$ is either alive or dead never both.
% \end{corollary}
% 

\subsection{Preliminaries on Well Structured Transition Systems}
The decidability of reachability for \rsd nets will be shown by appealing to the theory of
well-structured transition systems \cite{FinkelS01,AbdullaCJT00}.
The following results and definitions are from \cite{FinkelS01},  unless
differently specified. 

Recall that a \emph{quasi-order} (or, equivalently, preorder) is a reflexive
and transitive relation.

\begin{definition}[Well-quasi-order]
A \emph{well-quasi-order} (wqo) is a quasi-order $\leq$ over a
set $X$ such that, for any infinite sequence $x_0 , x_1 , x_2 \ldots \in X$, there exist indexes $i < j$
such that $x_i \leq x_j$.
\end{definition}

 Note that if $\leq$ is a wqo then any infinite sequence $x_0 , x_1 , x_2 , \ldots$ contains an infinite
increasing subsequence $x_{i_0} , x_{i_1} , x_{i_2} , \ldots$ (with $i_0 < i_1 < i_2 < \ldots$). 
Thus well-quasi-orders exclude the possibility of having infinite strictly decreasing sequences.


Here and in the following %$\rightarrow^{+}$ (resp. 
$\rightarrow^*$ denotes the 
%transitive (resp. the 
reflexive and transitive
%) 
closure of the relation $\rightarrow$.


\begin{definition}[Transition system]
\label{def:WSTS}
A \emph{transition system} is a structure $TS = (S, \rightarrow)$, where $S$ is a set of states
and $\rightarrow \subseteq  S \times S$ is a set of transitions. 
We define $Succ(s)$ as the set $\{s' \in S \mid s \rightarrow s' \}$
of immediate \emph{successors} of $s$. %We say that 
$TS$ is \emph{finitely branching} if, for each $s \in S$,
$Succ(s)$ is finite.
We also define $Pred(s)$ as the set $\{s' \in S \mid s' \rightarrow s\}$ of \emph{immediate predecessors} of $s$,
while $Pred^*(s)$ and $Pred^+(s)$ denote the sets $\{s \in S \mid s' \rightarrow^* s\}$ and  $\{s \in S \mid s' \rightarrow^+ s\}$, respectively, of \emph{predecessors} of $s$.
\end{definition}

\begin{newnotation}
In the rest of the paper, 
and with a slight abuse of notation,
we will  assume the expected point-wise extensions of definitions to sets. 
For instance, 
function $Succ$ just defined on states is extended to sets of states as:
 %, $Pred$, $Pred^*$ and  $Pred^+$
%will also be used  
%on sets, %by assuming 
%that in this case they are defined by 
%the point-wise extension of the above definitions, 
$Succ(S) = \bigcup_{s \in S} Succ(s)$.  
\end{newnotation}




The key tool to 
the decidability of 
%decide 
several properties of computations 
is the notion of \emph{well-structured transition system} \cite{FinkelS01,AbdullaCJT00}. 
This is a transition system equipped with a well-quasi-order on states
which is (upward) compatible with the transition relation. Here we will use a strong version 
of compatibility; hence the following definition.


\begin{definition}[Well-structured transition system] %with strong compatibility]
A \emph{well-struc\-tured transition system with strong compatibility} is a transition system 
$TS = (S, \rightarrow)$, equipped with a quasi-order $\leq$ on $S$, such that the two following conditions hold:
%\vspace{-2mm}
\begin{enumerate}
\item 
 $\leq$ is a well-quasi-order;
\item 
 $\leq$ is strongly (upward) compatible with $\rightarrow$, that is, for all $s_1 \leq t_1$ and all transitions
   $s_1 \rightarrow s_2$ , there exists a state $t_2$ such that $t_1 \rightarrow t_2$ and $s_2 \leq t_2$ holds.
\end{enumerate}
\end{definition}

The following theorem is a special case of Theorem 4.6 in \cite{FinkelS01} and will be used to obtain our decidability result.

\begin{theorem}\label{th:Finkel}
Let $TS = (S, \rightarrow, \leq)$ be a finitely branching, well-structured transition
system with strong compatibility, decidable $\leq$,  and computable $Succ$. Then the existence
of an infinite computation starting from a state $s \in S$ is decidable.
\end{theorem}

Given a quasi-order $\leq$ over $X$, an {\em upward-closed set} is a subset $I\subseteq X$ such that
the following holds: $\forall x,y\in X: (x\in I\wedge x\leq y)\Rightarrow y\in I$. Given $x\in X$, we define its upward closure as $\uparrow x = \{y\in X\mid x\leq y\}$. This notion can be extended to sets as expected: given a set $Y\subseteq X$ we define its upward closure as $\uparrow Y = \bigcup_{y\in Y}\uparrow y$. 

\begin{definition}[Finite basis]\label{d:finbas}
A {\em finite basis} of an upward-closed set $I$ is a finite set $B$ such that $I = \bigcup_{x\in B}\uparrow x$.
\end{definition}

%In our case t
The notion of basis is particularly important when considering 
the basis of the predecessor of a state in a transition system. More precisely, we are interested in  \emph{effective} pred-basis as defined below.

\begin{definition}[Effective pred-basis]\label{d:efpb}
A well-structured transition system has {\em effective pred-basis} if there exists an algorithm such that, for any state $s\in S$, it returns the set $pb(s)$ which is a finite basis of $\uparrow Pred(\uparrow s)$.
\end{definition}

The following proposition is a special case of Proposition 3.5 
in \cite{FinkelS01}.
\begin{proposition} \label{predcomp}
Let $TS = (S,\rightarrow,\leq)$ be a finitely branching,
well-structured transition system
with strong compatibility, decidable $\leq$ and effective pred-basis.
It is possible to compute a finite basis of $Pred^*(I)$ for any upward-closed set $I$
given via a finite basis.
\end{proposition}

% We will also need a result due to Higman \cite{Higman52} which allows to extend a well-quasi-order
% from a set $S$ to the set of the finite sequences on $S$. More precisely, given a set $S$ let
% us denote by $S^*$ the set of finite sequences built by using elements in $S$. 
% We can define a quasi-order on $S^*$ as follows.
% 
% \begin{definition}\label{def:eqwqo}
% Let $S$ be a set and $\leq$ a quasi-order over $S$. The relation $\leq_*$ over $S^*$
% is defined as follows. Let $t, u \in S^*$, with $t = t_1 t_2 \ldots t_m$ and $u = u_1 u_2 \ldots u_n$. 
% We have that $t \leq_* u$ if and only if there exists an injection $f$ from $\{1, 2, \ldots m \}$ 
% to $\{1, 2, \ldots n\}$ such that $t_i \leq u_{f (i)}$ and $f(i) < f(i+1)$ 
% for $i = 1, \ldots , m-1$.
% \end{definition}
% 
% The relation $\leq_*$ is clearly a quasi-order over $S^*$. 
% It is also a wqo, since we have the following result.
% 
% \begin{lemma}[Higman] %\cite{Higman52}] 
% \label{lem:Higman}
% Let $S$ be a set and $\leq$ a wqo over $S$. 
% Then %the relation 
% $\leq_*$ is a wqo over $S^*$.
% \end{lemma}

Finally we will use the following proposition, whose proof is immediate.

\begin{proposition}\label{prop:eqwqo}
Let $S$ be a finite set. Then the equality is a wqo over $S$.
\end{proposition}


% %Another 
% %An extension to the theory of wqo is needed in the rest of the paper. 
% We shall also appeal to the following result.
% In \cite{kruskal60}, Kruskal proved that a wqo on a set $S$ can be extended to the set of finite trees whose nodes have labels ranging in $S$; we refer to this as the set of trees \emph{over} $S$.
% We first define how to extend a quasi order on a set $S$ to the trees over $S$.
% If $t$ is a tree and $n$ a node in $t$, we denote with $label(n)$ the label of the node $n$.
% 
% \begin{definition}\label{def:prectr}
%   Let $S$ and $\leq$ be a set and a wqo over $S$, respectively. 
%   The relation $\leq^{\mathsf{tr}}$ on the set of
% trees over $S$ is defined as follows. Let $t, u$ be trees over $S$. We have that $t \leq^{\mathsf{tr}} u$ iff there
% exists an injection $f$ from the nodes of $t$ to the ones of $u$ such that:
% \begin{enumerate}
%  \item Let $m,n$ be nodes in $t$. If $m$ is an ancestor of $n$ then $f(m)$ is an ancestor of $f(n)$.
%  \item Let $m,n,p$ be nodes in $t$. If $p$ is the minimal common ancestor of $m$ and $n$ then $f(p)$ is the minimal common ancestor of $f(m)$ and $f(n)$.
%  \item Let $n$ be a node in $t$. Then $label(n) \leq label(f(n))$.
% \end{enumerate}
% \end{definition}
% 
% %Similarly as before t
% The relation $\leq^{tr}$ is  a quasi-order over the trees over $S$. 
% It is also a wqo, since we have the following result.
% 
% \begin{theorem}[Kruskal \cite{kruskal60}]\label{lem:kruskal}
%    Let $S$ be a set and $\leq$ a wqo over $S$. Then, the relation $\leq^{tr}$ 
% is a wqo on the set of trees over $S$.
% \end{theorem}
% 
% 

% 



\subsection{Reachability is decidable}
\begin{definition}[$\preceq$] \label{def:ordering}
 Given two markings 
  $$
  \begin{array}{lcl}
   m&=& (z, \tuple{\bool_1, \refr_1, \birth_1}, \dots , \tuple{\bool_n, \refr_n, \birth_n} ) \\
   m'&=& (z', \tuple{\bool_1', \refr_1', \birth_1'}, \dots , \tuple{\bool_n', \refr_n', \birth_n'} )
  \end{array}
  $$
  we say that $m \preceq m'$ iff
  \begin{enumerate}
   \item $z \leq z'$;
   \item $\forall i$ if $\bool_i = \bool_i' = 1$ then $z-\refr_i = z' - \refr_i'$ and $z-\birth_i \leq z' - \birth_i'$;
   \item $\forall i$ if $\bool_i = \bool_i' = 0$ then $z-\birth_i \leq z' -te \birth_i'$.
   \end{enumerate}
\todo{Non mi sembra vada bene, i $\bool$ devono essere uguali, non è un implica ma un and}
\end{definition}


\begin{lemma}
 $\preceq$ is a well-quasi-order over the set of markings $M$.
\end{lemma}
\begin{proof}
 The proof follows by observing that $\preceq$ is the composition of two well-quasi-orders: $\leq$ over $\nat$ and equality over the finite set $[0..max_i(\life(S_i))]$ (Proposition \ref{prop:eqwqo}). Indeed, notice that $z-\refr_i$ will always be contained in that interval, as no species $S_i$ can live more than $\life(S_i)$ time units. 
\end{proof}

\begin{lemma}
 $\preceq$ is strongly compatible wrt $\rightarrow$
\end{lemma}
\begin{proof}
 Let $\firing{m_1}{t}{m_2}$ and $m_1 \preceq m_1'$, we want to show that there exists an $m_2'$ such that $\firing{m_1'}{t}{m_2'}$ and $m_2 \preceq m_2'$.
  The proof proceeds by a case analysis on the type of  transition $t$. By construction there are two types of transition: the transition of the clock $t_c$ and transitions that correspond to reactions $t_r$.
 \begin{description}
  \item[$t_c$] This transition is always enabled. Thus it can be performed with marking $m_1'$, the only interesting case happens when one of the species changes its status from available to unavailable, the switch is guaranteed to happen in $m_1'$ by condition (2) of Definition \ref{def:ordering} thus implying that $m_2 \preceq m_2'$ and concluding the analysis of this case.
  \item[$t_r$] This transition is enabled iff $$\bigwedge_{S_i \in (R \cup I)}(z-\birth_i \geq \dur(r)) \ \wedge 
\bigwedge_{P_k \in P}\big [ (\bool_k=0 \wedge \birth_k' = z) \vee (\bool_k=1 \wedge \birth_k' = \birth_k) \big].$$
Notice that as $m \preceq m'$ all reactants (resp. inhibitors) in $m$ are reactants (resp. inhibitors in $m'$ and conditions (2) (resp. (3)) of Definition \ref{def:ordering} guarantees that if $z-\birth_i \geq \dur(r))$ then  $z'-\birth_i' \geq \dur(r))$.
Thus completing the analysis of this case and the proof.
\todo{espandere e più preciso caso clock}
 \end{description}
\end{proof}



